all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$P$($e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$e$:es{-}E(${\it es}$). es{-}le(${\it es}$; $e_{1}$; $e$) $\Rightarrow$ es{-}locl(${\it es}$; $e$; $e_{2}$) $\Rightarrow$ $P$($e$)